YES(O(1),O(n^1)) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict Trs: { not(true()) -> false() , not(false()) -> true() , evenodd(x, 0()) -> not(evenodd(x, s(0()))) , evenodd(0(), s(0())) -> false() , evenodd(s(x), s(0())) -> evenodd(x, 0()) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. Trs: { evenodd(0(), s(0())) -> false() } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^1)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- TcT has computed the following constructor-based matrix interpretation satisfying not(EDA). [not](x1) = [1] x1 + [0] [true] = [0] [false] = [0] [evenodd](x1, x2) = [2] x1 + [1] x2 + [1] [0] = [0] [s](x1) = [1] x1 + [0] This order satisfies the following ordering constraints: [not(true())] = [0] >= [0] = [false()] [not(false())] = [0] >= [0] = [true()] [evenodd(x, 0())] = [2] x + [1] >= [2] x + [1] = [not(evenodd(x, s(0())))] [evenodd(0(), s(0()))] = [1] > [0] = [false()] [evenodd(s(x), s(0()))] = [2] x + [1] >= [2] x + [1] = [evenodd(x, 0())] We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict Trs: { not(true()) -> false() , not(false()) -> true() , evenodd(x, 0()) -> not(evenodd(x, s(0()))) , evenodd(s(x), s(0())) -> evenodd(x, 0()) } Weak Trs: { evenodd(0(), s(0())) -> false() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 2' to orient following rules strictly. Trs: { evenodd(s(x), s(0())) -> evenodd(x, 0()) } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^1)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- TcT has computed the following constructor-based matrix interpretation satisfying not(EDA) and not(IDA(1)). [not](x1) = [1 0] x1 + [0] [0 0] [0] [true] = [0] [0] [false] = [0] [0] [evenodd](x1, x2) = [2 2] x1 + [2 0] x2 + [0] [0 0] [0 0] [0] [0] = [0] [0] [s](x1) = [1 2] x1 + [0] [0 0] [2] This order satisfies the following ordering constraints: [not(true())] = [0] [0] >= [0] [0] = [false()] [not(false())] = [0] [0] >= [0] [0] = [true()] [evenodd(x, 0())] = [2 2] x + [0] [0 0] [0] >= [2 2] x + [0] [0 0] [0] = [not(evenodd(x, s(0())))] [evenodd(0(), s(0()))] = [0] [0] >= [0] [0] = [false()] [evenodd(s(x), s(0()))] = [2 4] x + [4] [0 0] [0] > [2 2] x + [0] [0 0] [0] = [evenodd(x, 0())] We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict Trs: { not(true()) -> false() , not(false()) -> true() , evenodd(x, 0()) -> not(evenodd(x, s(0()))) } Weak Trs: { evenodd(0(), s(0())) -> false() , evenodd(s(x), s(0())) -> evenodd(x, 0()) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 2' to orient following rules strictly. Trs: { evenodd(x, 0()) -> not(evenodd(x, s(0()))) } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^1)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- TcT has computed the following constructor-based matrix interpretation satisfying not(EDA) and not(IDA(1)). [not](x1) = [1 0] x1 + [0] [0 0] [0] [true] = [0] [0] [false] = [0] [0] [evenodd](x1, x2) = [2 0] x1 + [2 3] x2 + [2] [0 0] [0 0] [0] [0] = [0] [1] [s](x1) = [1 0] x1 + [1] [0 0] [0] This order satisfies the following ordering constraints: [not(true())] = [0] [0] >= [0] [0] = [false()] [not(false())] = [0] [0] >= [0] [0] = [true()] [evenodd(x, 0())] = [2 0] x + [5] [0 0] [0] > [2 0] x + [4] [0 0] [0] = [not(evenodd(x, s(0())))] [evenodd(0(), s(0()))] = [4] [0] > [0] [0] = [false()] [evenodd(s(x), s(0()))] = [2 0] x + [6] [0 0] [0] > [2 0] x + [5] [0 0] [0] = [evenodd(x, 0())] We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict Trs: { not(true()) -> false() , not(false()) -> true() } Weak Trs: { evenodd(x, 0()) -> not(evenodd(x, s(0()))) , evenodd(0(), s(0())) -> false() , evenodd(s(x), s(0())) -> evenodd(x, 0()) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 2' to orient following rules strictly. Trs: { not(true()) -> false() , not(false()) -> true() } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^1)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- TcT has computed the following constructor-based matrix interpretation satisfying not(EDA) and not(IDA(1)). [not](x1) = [1 0] x1 + [1] [0 0] [0] [true] = [0] [0] [false] = [0] [0] [evenodd](x1, x2) = [2 0] x1 + [1 1] x2 + [0] [0 0] [0 0] [0] [0] = [1] [3] [s](x1) = [1 0] x1 + [1] [0 0] [0] This order satisfies the following ordering constraints: [not(true())] = [1] [0] > [0] [0] = [false()] [not(false())] = [1] [0] > [0] [0] = [true()] [evenodd(x, 0())] = [2 0] x + [4] [0 0] [0] > [2 0] x + [3] [0 0] [0] = [not(evenodd(x, s(0())))] [evenodd(0(), s(0()))] = [4] [0] > [0] [0] = [false()] [evenodd(s(x), s(0()))] = [2 0] x + [4] [0 0] [0] >= [2 0] x + [4] [0 0] [0] = [evenodd(x, 0())] We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak Trs: { not(true()) -> false() , not(false()) -> true() , evenodd(x, 0()) -> not(evenodd(x, s(0()))) , evenodd(0(), s(0())) -> false() , evenodd(s(x), s(0())) -> evenodd(x, 0()) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded Hurray, we answered YES(O(1),O(n^1))